COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	HELP
C00017 ENDMK
C⊗;
HELP
"This program is designed to be used as a tool for verification
of properties of PASCAL programs presented to it, along with
lemmas about those programs.  The most commonly used upper level
command is PARSE.  Type (HELP WHAT) for a list of help commands.
For help on topic X, assuming help data exists, type (HELP X)."

WHAT
"HELP messages are available for the following:
BUG
DEDUCE
DOCUMENTATION
DUMPSYMBOLS
DUMPVCS
INTEGERS
LIMERICK
LISP
LOADSYMBOLS
LOADVCS
MANUAL
PARSE
PREVIOUS
PRINTVC
RESIMPLIFY
SETAUTO
SETGOALDEPTH
SETLIMERICK
SETMANUAL
SIMPLIFY
TRACEPROOF
UNSETLIMERICK
UNTRACEPROOF
"

BUG
"The BUG feature is provided to help verifier hackers make changes
to syntax, semantics, etc.  There are two user commands,
(SETBUG <number>) and (RESETBUG <number>), which set and then reset
the bug with the appropriate number.  See MEMO[VCG,RAK] to see which
bugs currently exist and what they do."

DEDUCE
"The DEDUCE instruction is designed to assist checking out the
provers in the verifier.  It operates at the highest level like
PARSE; i.e. (DEDUCE) will expect input from the terminal and
(DEDUCE <file>) looks for <file> (HELP PARSE) will tell you about
file formats.  DEDUCE expects a single basis expression terminated
with a ';.'(note that there is no keyword at the start and that both
the semicolon and period, in that order, must be at the end). It will
process this into internal format, call INFER, and print out the
result on the terminal.  If BUG#4 is set, it will also print out the
internal format being passed to INFER."

DOCUMENTATION
"Documentation on the verifier or portions thereof exists on the
following files (at least):
MEMO[VCG,RAK] about the parser, Pascal, etc.
SSEM[VCG,RAK] --page 2 explains the structure of the symbol table
SYNTAX.N[VER,WLS]--rulefile syntax, internal tree structure
"

DUMPSYMBOLS
"The command DUMPSYMBOLS is optionally followed by a file in the
same format as PARSE.  It instructs the parser to dump code to that
file that will permit reloading the symbol table environment of all
the procedures in the file.  (DUMPSYMBOLS) turns off dumping.  So
does any subsequent attempt to load a symbol table file.  See
LOADSYMBOLS for information on how to load a symbol table."

DUMPVCS
"The command DUMPVCS is followed by a file in the same format as
PARSE.  It instructs the parser to dump code to that file that
will permit reloading the verification conditions currently
known to the system.  See LOADVCS for information on how to load
in VCs."

INTEGERS
"The command (INTEGERS) tells the verifier that all the numbers it
will be dealing with henceforth in this session are integers or 
subsets (not reals).  This may permit some deductions that are not
valid for general real arithmetic, and thus facilitates integer
proofs."

LIMERICK
"(LIMERICK) prints out a randomly chosen and invariably tasteless
limerick.   You are adivsed to hide your channel before using the
limerick generator.   Limericks may also be automatically generated
during simplification; see (SETLIMERICK)"

LISP
"Although this is primarily a program verifier, it exists in a
LISP 1.6 environment.  This means that the general facilities of
such LISP are available.  Some that may be of interest are (GCGAG T),
which causes a printout every time a garbage collection takes place.
This may help indicate the need for running in a larger core image.
It can be turned off by (GCGAG NIL).  Also, (GCTIME) prints out
the processor time thus far spent in garbage collection."

LOADSYMBOLS
"The command LOADSYMBOLS must be followed by two items: first a
procedure name and then a file.  The system will turn off symbol
table dumping (if it is on), clear the symbol table, and then attempt
to load the symbol table environment of the procedure specified from
the file given.  The format of the file name is the same as that of
the PARSE command. See DUMPSYMBOLS for information on how to create
a file that contains symbol table information."

LOADVCS
"The command LOADVCS must be followed by a file in the same format
as that of the PARSE command.  The system will delete all currently
known verification conditions, and then attempt to load in 
verification conditions dumped to the file named in this command.
See DUMPVCS for information on how to create a file that contains
verification conditions."

MANUAL
"In manual mode, type any of the following:
 
↑  : Leave formula as is; back up and continue.
↑↑ : Leave formula as is; back up to top level.
↓  : Prove formula without interactive guidance; back up if provable.
↓↑ : Prove formula without interactive guidance; back up.
?  : Print out facts known in this context.

( <toplevel command to VERIFY> )
   : Execute the command, then continue the proof.  For example,
     in the middle of a proof you can add a new rule as in

          (PARSE)RULEFILE R1(Y): INFER P(X) FROM Q(X,Y);.

     The rule is added and the proof continues.  Hopefully no
     VERIFY command can cause problems, but to avoid confusion,
     INFER does not allow you to (SIMPLIFY) or (DEDUCE).

<rulename> ( <list of expressions> ) .
   : Apply the inference rule with name <rulename>.   The 
     ( <list of expressions> ) is optional; if it appears, the
     expressions are used to instantiate those free variables 
     specified in the definition of the rule.  For instance, given

		R1(Y): INFER P(X) FROM Q(X,Y);

     then if you type R1(A). Y is instantiated to A.  If you type 
     R1. then the pattern matcher will try to find an appropriate 
     instantiation for Y.  
     NOTE: a period must always come at the end."
 
PARSE
"The command (PARSE) accepts input from the teletype. (PARSE X)
will try to take input from the file X.  Here are some examples
for taking files with two word names and from another directory
(here p,pn is programmer,project): (PARSE (X.Y)), (PARSE (P,PN)X),
and (PARSE (P,PN)(X.Y))  .
The parser calls the verification condition generator, but does
not do simplification.  For this, the command SIMPLIFY must be
used. The syntactic scan and semantic routines should NEVER
bomb out, no matter what string you give them.  If they do,
send a note to RAK and SAVE the program!!!"

PREVIOUS
"The command (PREVIOUS <positive integer>) has meaning when a
syntax scan finds a syntax error.  It will print out as many
tokens preceding the syntax error as it is asked (if there are
that many).  (PREVIOUS 10) is called in the errorhandling.  As
the number of tokens requested increases, time to find them can
go up alarmingly. After an error and before parsing something
else, previous may be called as many times as desired."

PRINTVC
"The command PRINTVC is used to output unsimplified verfication
conditions.  (PRINTVC) prints out all of these on the
terminal.  (PRINTVC X) prints out all of the VC's for procedure
X.  (PRINTVC X 3) prints the third VC for procedure X.
(PRINTVC (F)) prints out all VC's to file F, which is replaced
if it was previously present.  (PRINTVC (F) X) prints out all
VC's for procedure X on file F.
The outer block of a program is currently called MAIN. It will
remove VC's for a procedure named MAIN, if one is present!"

RESIMPLIFY
"(RESIMPLIFY) sends the most-recently simplified formula back
through the prover for (hopefully) further simplification."

SETAUTO
"(SETAUTO) is the default mode for the prover.   It is non-interactive.
The alternative mode of proof is (SETMANUAL)"

SETLIMERICK
"(SETLIMERICK) turns on the automatic limerick generator.   After the
first eight CPU seconds of simplification, a randomly chosen limerick
in distinctly questionable taste is printed out.   Further limericks
are printed out at exponentially increasing intervals, i.e. 16 CPU secs,
32 secs, 64 secs, etc.    (UNSETLIMERICK) turns off the generator."

SETMANUAL
"(SETMANUAL) is the interactive mode of proof.   The default mode is
(SETAUTO).   In manual mode, you are only asked for guidance if
the prover is unable to prove an atomic formula using everything
at its disposal except inference rules.  The possible commands in
manual mode can be seen by typing ? in manual mode or (HELP MANUAL)"

SETGOALDEPTH
"The command (SETGOALDEPTH <integer>) controls how deep inference
rule applications are made in attempting to prove something.  
The default is 5.  If the verifier does not seem to be proving 
a complex fact for which adequate axioms are available, increasing
GOALDEPTH may help (generally at a considerable increase in 
execution time)."

SIMPLIFY
"The command SIMPLIFY is used to call the simplifier and output
simplified verification conditions.  The procedure and output
file specifications are the same as for PRINTVC.  Use
(HELP PRINTVC) to see these conventions."

TRACEPROOF
"The command (TRACEPROOF) prints out trace information keeping
it to a mininum. It presently prints out the known facts
(antecedent) only when a new context is entered.   Other than that,
it just prints out the atomic formulas to be proved and why they
are proved or rejected.   (UNTRACEPROOF) turns the tracer off."

UNSETLIMERICK
"(UNSETLIMERICK) turns off the limerick generator.   See (SETLIMERICK)"

UNTRACEPROOF
"(UNTRACEPROOF) turns off the printing of trace information during
simplification.  (HELP TRACEPROOF) for details on trace routine"

END